(set-logic QF_LRA)
(declare-fun v1 () Bool)
(push 1)
(declare-fun v99 () Bool)
(declare-fun v98 () Bool)
(push 1)
(declare-fun v97 () Bool)
(declare-fun v96 () Bool)
(declare-fun v95 () Bool)
(declare-fun r99 () Real)
(declare-fun v94 () Bool)
(declare-fun v93 () Bool)
(pop 1)
(declare-fun v97 () Bool)
(declare-fun r99 () Real)
(pop 1)
(declare-fun v16 () Bool)
(assert (= v16 v1))
(push 1)
(declare-fun v852 () Bool)
(declare-fun r359 () Real)
(declare-fun r358 () Real)
(declare-fun v851 () Bool)
(declare-fun v850 () Bool)
(declare-fun r357 () Real)
(declare-fun v849 () Bool)
(declare-fun v848 () Bool)
(declare-fun v847 () Bool)
(declare-fun r356 () Real)
(declare-fun v846 () Bool)
(declare-fun v845 () Bool)
(declare-fun v844 () Bool)
(declare-fun r355 () Real)
(push 1)
(declare-fun v99 () Bool)
(pop 1)
(declare-fun v843 () Bool)
(push 1)
(declare-fun v842 () Bool)
(declare-fun v841 () Bool)
(declare-fun r99 () Real)
(push 1)
(declare-fun v840 () Bool)
(push 1)
(declare-fun v99 () Bool)
(declare-fun v98 () Bool)
(declare-fun v97 () Bool)
(declare-fun r98 () Real)
(declare-fun v96 () Bool)
(declare-fun r97 () Real)
(push 1)
(declare-fun v95 () Bool)
(push 1)
(declare-fun v94 () Bool)
(declare-fun r96 () Real)
(pop 1)
(declare-fun v94 () Bool)
(declare-fun r96 () Real)
(pop 1)
(declare-fun v95 () Bool)
(declare-fun r96 () Real)
(push 1)
(push 1)
(declare-fun v94 () Bool)
(declare-fun v93 () Bool)
(push 1)
(declare-fun v92 () Bool)
(declare-fun r95 () Real)
(declare-fun v91 () Bool)
(declare-fun r94 () Real)
(declare-fun v90 () Bool)
(declare-fun r93 () Real)
(push 1)
(declare-fun r92 () Real)
(push 1)
(declare-fun v89 () Bool)
(declare-fun v88 () Bool)
(declare-fun r91 () Real)
(push 1)
(declare-fun v87 () Bool)
(declare-fun r90 () Real)
(declare-fun v86 () Bool)
(push 1)
(declare-fun r89 () Real)
(declare-fun v85 () Bool)
(declare-fun v84 () Bool)
(declare-fun v839 () Bool)
(declare-fun r88 () Real)
(push 1)
(declare-fun r87 () Real)
(declare-fun v838 () Bool)
(declare-fun v837 () Bool)
(declare-fun v836 () Bool)
(pop 1)
(pop 1)
(declare-fun v85 () Bool)
(declare-fun r89 () Real)
(declare-fun r88 () Real)
(declare-fun v84 () Bool)
(pop 1)
(declare-fun r90 () Real)
(pop 1)
(declare-fun v89 () Bool)
(declare-fun v88 () Bool)
(pop 1)
(declare-fun v89 () Bool)
(push 1)
(declare-fun v88 () Bool)
(declare-fun v87 () Bool)
(declare-fun r92 () Real)
(declare-fun v86 () Bool)
(declare-fun r91 () Real)
(declare-fun v85 () Bool)
(pop 1)
(declare-fun v88 () Bool)
(declare-fun r92 () Real)
(declare-fun v87 () Bool)
(declare-fun r91 () Real)
(declare-fun v86 () Bool)
(declare-fun v85 () Bool)
(push 1)
(declare-fun v84 () Bool)
(declare-fun r90 () Real)
(pop 1)
(declare-fun v84 () Bool)
(pop 1)
(declare-fun v92 () Bool)
(declare-fun v91 () Bool)
(pop 1)
(declare-fun r95 () Real)
(push 1)
(declare-fun v94 () Bool)
(pop 1)
(declare-fun v94 () Bool)
(declare-fun r94 () Real)
(push 1)
(declare-fun r93 () Real)
(declare-fun v93 () Bool)
(pop 1)
(pop 1)
(declare-fun v94 () Bool)
(declare-fun r95 () Real)
(push 1)
(declare-fun v93 () Bool)
(pop 1)
(pop 1)
(declare-fun v90 () Bool)
(declare-fun r98 () Real)
(push 1)
(push 1)
(declare-fun v99 () Bool)
(declare-fun v98 () Bool)
(declare-fun v97 () Bool)
(declare-fun v96 () Bool)
(declare-fun v95 () Bool)
(declare-fun v94 () Bool)
(declare-fun r97 () Real)
(pop 1)
(declare-fun v92 () Bool)
(declare-fun v91 () Bool)
(declare-fun r97 () Real)
(declare-fun v86 () Bool)
(declare-fun r96 () Real)
(declare-fun v87 () Bool)
(declare-fun v88 () Bool)
(declare-fun r95 () Real)
(push 1)
(declare-fun v89 () Bool)
(declare-fun r94 () Real)
(push 1)
(declare-fun v99 () Bool)
(declare-fun r93 () Real)
(push 1)
(declare-fun v98 () Bool)
(pop 1)
(declare-fun v98 () Bool)
(pop 1)
(declare-fun v93 () Bool)
(declare-fun v94 () Bool)
(declare-fun v95 () Bool)
(push 1)
(declare-fun v96 () Bool)
(push 1)
(declare-fun v97 () Bool)
(declare-fun v98 () Bool)
(declare-fun v99 () Bool)
(declare-fun r93 () Real)
(pop 1)
(declare-fun v99 () Bool)
(declare-fun v98 () Bool)
(pop 1)
(pop 1)
(declare-fun v99 () Bool)
(declare-fun r94 () Real)
(push 1)
(declare-fun v98 () Bool)
(push 1)
(declare-fun v97 () Bool)
(declare-fun r93 () Real)
(push 1)
(declare-fun v96 () Bool)
(declare-fun r92 () Real)
(declare-fun v95 () Bool)
(declare-fun v94 () Bool)
(pop 1)
(declare-fun v96 () Bool)
(pop 1)
(declare-fun v97 () Bool)
(declare-fun v96 () Bool)
(pop 1)
(declare-fun v98 () Bool)
(declare-fun v97 () Bool)
(declare-fun v96 () Bool)
(declare-fun v95 () Bool)
(declare-fun r93 () Real)
(pop 1)
(declare-fun v99 () Bool)
(declare-fun r97 () Real)
(declare-fun v98 () Bool)
(declare-fun v97 () Bool)
(declare-fun v96 () Bool)
(declare-fun v95 () Bool)
(declare-fun r96 () Real)
(push 1)
(declare-fun v94 () Bool)
(pop 1)
(declare-fun v94 () Bool)
(declare-fun r95 () Real)
(push 1)
(declare-fun v93 () Bool)
(declare-fun r94 () Real)
(declare-fun v92 () Bool)
(pop 1)
(declare-fun v93 () Bool)
(declare-fun r94 () Real)
(declare-fun v92 () Bool)
(declare-fun v91 () Bool)
(pop 1)
(declare-fun v99 () Bool)
(push 1)
(declare-fun v98 () Bool)
(declare-fun r98 () Real)
(declare-fun v97 () Bool)
(declare-fun r90 () Real)
(push 1)
(declare-fun v96 () Bool)
(declare-fun v95 () Bool)
(declare-fun v94 () Bool)
(push 1)
(declare-fun v93 () Bool)
(declare-fun v92 () Bool)
(push 1)
(push 1)
(declare-fun v91 () Bool)
(declare-fun v90 () Bool)
(declare-fun r97 () Real)
(push 1)
(declare-fun v89 () Bool)
(push 1)
(declare-fun v88 () Bool)
(declare-fun r96 () Real)
(push 1)
(declare-fun r95 () Real)
(pop 1)
(pop 1)
(declare-fun r96 () Real)
(push 1)
(declare-fun v88 () Bool)
(declare-fun v87 () Bool)
(declare-fun r95 () Real)
(pop 1)
(declare-fun r95 () Real)
(declare-fun v88 () Bool)
(declare-fun v87 () Bool)
(declare-fun r94 () Real)
(pop 1)
(declare-fun v89 () Bool)
(pop 1)
(declare-fun v91 () Bool)
(push 1)
(declare-fun v90 () Bool)
(declare-fun v89 () Bool)
(push 1)
(declare-fun v88 () Bool)
(declare-fun r97 () Real)
(push 1)
(declare-fun r96 () Real)
(declare-fun v87 () Bool)
(push 1)
(declare-fun v86 () Bool)
(declare-fun v85 () Bool)
(declare-fun r95 () Real)
(push 1)
(declare-fun v840 () Bool)
(declare-fun r94 () Real)
(pop 1)
(declare-fun v840 () Bool)
(declare-fun r94 () Real)
(push 1)
(declare-fun v84 () Bool)
(declare-fun r93 () Real)
(declare-fun v839 () Bool)
(push 1)
(declare-fun r92 () Real)
(declare-fun v838 () Bool)
(declare-fun r91 () Real)
(push 1)
(declare-fun v837 () Bool)
(pop 1)
(pop 1)
(declare-fun v838 () Bool)
(pop 1)
(declare-fun v84 () Bool)
(declare-fun v839 () Bool)
(pop 1)
(declare-fun v86 () Bool)
(declare-fun v85 () Bool)
(declare-fun v840 () Bool)
(declare-fun r95 () Real)
(push 1)
(declare-fun v84 () Bool)
(pop 1)
(declare-fun v84 () Bool)
(declare-fun v839 () Bool)
(declare-fun r94 () Real)
(push 1)
(declare-fun v838 () Bool)
(declare-fun v837 () Bool)
(pop 1)
(declare-fun v838 () Bool)
(declare-fun v837 () Bool)
(declare-fun v836 () Bool)
(pop 1)
(declare-fun v87 () Bool)
(declare-fun v86 () Bool)
(declare-fun r96 () Real)
(pop 1)
(declare-fun r97 () Real)
(pop 1)
(declare-fun v90 () Bool)
(declare-fun v89 () Bool)
(declare-fun r97 () Real)
(declare-fun v88 () Bool)
(declare-fun v87 () Bool)
(pop 1)
(declare-fun v91 () Bool)
(declare-fun v90 () Bool)
(declare-fun r97 () Real)
(declare-fun v89 () Bool)
(declare-fun v88 () Bool)
(declare-fun r96 () Real)
(declare-fun v87 () Bool)
(declare-fun r95 () Real)
(pop 1)
(declare-fun v93 () Bool)
(declare-fun v92 () Bool)
(declare-fun v91 () Bool)
(declare-fun v90 () Bool)
(declare-fun v89 () Bool)
(declare-fun v88 () Bool)
(declare-fun r97 () Real)
(declare-fun r95 () Real)
(declare-fun v87 () Bool)
(declare-fun v86 () Bool)
(declare-fun v85 () Bool)
(declare-fun v840 () Bool)
(declare-fun v84 () Bool)
(push 1)
(declare-fun v839 () Bool)
(pop 1)
(declare-fun v839 () Bool)
(declare-fun v838 () Bool)
(declare-fun r96 () Real)
(declare-fun v837 () Bool)
(pop 1)
(declare-fun v96 () Bool)
(declare-fun r97 () Real)
(pop 1)
(declare-fun v98 () Bool)
(declare-fun r98 () Real)
(pop 1)
(declare-fun v99 () Bool)
(declare-fun v98 () Bool)
(declare-fun v97 () Bool)
(declare-fun r99 () Real)
(declare-fun v96 () Bool)
(declare-fun v95 () Bool)
(declare-fun r98 () Real)
(pop 1)
(assert false)
(push 1)
(declare-fun v99 () Bool)
(declare-fun v98 () Bool)
(declare-fun v97 () Bool)
(push 1)
(declare-fun v96 () Bool)
(push 1)
(declare-fun v95 () Bool)
(declare-fun v94 () Bool)
(declare-fun v93 () Bool)
(pop 1)
(declare-fun v95 () Bool)
(pop 1)
(declare-fun v96 () Bool)
(declare-fun v95 () Bool)
(declare-fun r99 () Real)
(declare-fun v94 () Bool)
(declare-fun r98 () Real)
(declare-fun v93 () Bool)
(declare-fun v92 () Bool)
(push 1)
(declare-fun r97 () Real)
(declare-fun v91 () Bool)
(declare-fun r96 () Real)
(pop 1)
(declare-fun r97 () Real)
(pop 1)
(push 1)
(declare-fun v99 () Bool)
(declare-fun r99 () Real)
(push 1)
(declare-fun r98 () Real)
(push 1)
(declare-fun v98 () Bool)
(pop 1)
(declare-fun r97 () Real)
(pop 1)
(declare-fun v98 () Bool)
(declare-fun r98 () Real)
(declare-fun v97 () Bool)
(push 1)
(declare-fun v96 () Bool)
(push 1)
(declare-fun v95 () Bool)
(declare-fun v94 () Bool)
(declare-fun v93 () Bool)
(declare-fun r97 () Real)
(pop 1)
(declare-fun v95 () Bool)
(declare-fun v94 () Bool)
(push 1)
(declare-fun v93 () Bool)
(declare-fun v92 () Bool)
(declare-fun r97 () Real)
(push 1)
(push 1)
(declare-fun v91 () Bool)
(declare-fun v90 () Bool)
(declare-fun r96 () Real)
(push 1)
(declare-fun v89 () Bool)
(declare-fun r95 () Real)
(declare-fun v88 () Bool)
(pop 1)
(declare-fun v89 () Bool)
(pop 1)
(declare-fun v91 () Bool)
(pop 1)
(declare-fun v91 () Bool)
(push 1)
(declare-fun v90 () Bool)
(declare-fun r96 () Real)
(pop 1)
(declare-fun v90 () Bool)
(push 1)
(declare-fun v89 () Bool)
(pop 1)
(declare-fun v89 () Bool)
(declare-fun v88 () Bool)
(declare-fun v87 () Bool)
(declare-fun v86 () Bool)
(declare-fun v852 () Bool)
(declare-fun v851 () Bool)
(push 1)
(declare-fun v850 () Bool)
(declare-fun r96 () Real)
(declare-fun v85 () Bool)
(pop 1)
(declare-fun v850 () Bool)
(declare-fun r96 () Real)
(pop 1)
(declare-fun v93 () Bool)
(declare-fun v92 () Bool)
(declare-fun v91 () Bool)
(declare-fun v90 () Bool)
(declare-fun r97 () Real)
(pop 1)
(declare-fun v96 () Bool)
(declare-fun r97 () Real)
(declare-fun v95 () Bool)
(declare-fun r96 () Real)
(declare-fun v94 () Bool)
(declare-fun v93 () Bool)
(declare-fun v92 () Bool)
(declare-fun v91 () Bool)
(declare-fun v90 () Bool)
(declare-fun r95 () Real)
(declare-fun v89 () Bool)
(push 1)
(declare-fun v88 () Bool)
(push 1)
(declare-fun v87 () Bool)
(pop 1)
(declare-fun r94 () Real)
(pop 1)
(declare-fun v88 () Bool)
(declare-fun v87 () Bool)
(declare-fun v86 () Bool)
(declare-fun v852 () Bool)
(declare-fun r94 () Real)
(declare-fun v851 () Bool)
(declare-fun v850 () Bool)
(push 1)
(declare-fun v85 () Bool)
(push 1)
(declare-fun v849 () Bool)
(declare-fun v848 () Bool)
(declare-fun v847 () Bool)
(push 1)
(declare-fun v846 () Bool)
(declare-fun r93 () Real)
(push 1)
(declare-fun v845 () Bool)
(declare-fun r92 () Real)
(push 1)
(declare-fun r91 () Real)
(declare-fun v844 () Bool)
(declare-fun v843 () Bool)
(declare-fun v842 () Bool)
(push 1)
(declare-fun v841 () Bool)
(declare-fun v840 () Bool)
(pop 1)
(declare-fun v841 () Bool)
(declare-fun v840 () Bool)
(declare-fun r90 () Real)
(declare-fun r89 () Real)
(push 1)
(declare-fun v84 () Bool)
(declare-fun v839 () Bool)
(declare-fun r88 () Real)
(push 1)
(declare-fun r87 () Real)
(declare-fun v838 () Bool)
(push 1)
(declare-fun v837 () Bool)
(declare-fun v836 () Bool)
(declare-fun r69 () Real)
(declare-fun v835 () Bool)
(declare-fun r359 () Real)
(pop 1)
(declare-fun v837 () Bool)
(declare-fun r69 () Real)
(declare-fun v836 () Bool)
(declare-fun r359 () Real)
(declare-fun r358 () Real)
(declare-fun v835 () Bool)
(pop 1)
(declare-fun v838 () Bool)
(declare-fun v837 () Bool)
(push 1)
(declare-fun r87 () Real)
(pop 1)
(pop 1)
(declare-fun v84 () Bool)
(declare-fun v839 () Bool)
(pop 1)
(declare-fun v844 () Bool)
(declare-fun r91 () Real)
(push 1)
(declare-fun r90 () Real)
(push 1)
(declare-fun v843 () Bool)
(declare-fun v842 () Bool)
(declare-fun v841 () Bool)
(push 1)
(push 1)
(declare-fun v840 () Bool)
(pop 1)
(declare-fun v840 () Bool)
(declare-fun r89 () Real)
(declare-fun v84 () Bool)
(pop 1)
(declare-fun v840 () Bool)
(declare-fun v84 () Bool)
(declare-fun r89 () Real)
(push 1)
(push 1)
(declare-fun v839 () Bool)
(push 1)
(declare-fun r88 () Real)
(declare-fun v838 () Bool)
(declare-fun v837 () Bool)
(declare-fun r87 () Real)
(push 1)
(push 1)
(declare-fun v836 () Bool)
(declare-fun r69 () Real)
(declare-fun v835 () Bool)
(declare-fun r359 () Real)
(pop 1)
(declare-fun v836 () Bool)
(declare-fun v835 () Bool)
(declare-fun r69 () Real)
(pop 1)
(declare-fun r69 () Real)
(pop 1)
(declare-fun v838 () Bool)
(declare-fun r88 () Real)
(push 1)
(declare-fun v837 () Bool)
(pop 1)
(pop 1)
(declare-fun v839 () Bool)
(pop 1)
(declare-fun r88 () Real)
(push 1)
(declare-fun v839 () Bool)
(pop 1)
(declare-fun v839 () Bool)
(push 1)
(declare-fun v838 () Bool)
(declare-fun v837 () Bool)
(pop 1)
(declare-fun v838 () Bool)
(push 1)
(declare-fun v837 () Bool)
(declare-fun v836 () Bool)
(pop 1)
(pop 1)
(declare-fun v843 () Bool)
(push 1)
(declare-fun v842 () Bool)
(declare-fun r89 () Real)
(declare-fun v841 () Bool)
(pop 1)
(declare-fun v842 () Bool)
(declare-fun r89 () Real)
(declare-fun v841 () Bool)
(declare-fun r88 () Real)
(pop 1)
(declare-fun v843 () Bool)
(declare-fun v842 () Bool)
(pop 1)
(declare-fun v845 () Bool)
(declare-fun v844 () Bool)
(declare-fun v843 () Bool)
(pop 1)
(declare-fun v846 () Bool)
(push 1)
(declare-fun v845 () Bool)
(push 1)
(declare-fun r93 () Real)
(pop 1)
(declare-fun v844 () Bool)
(declare-fun v843 () Bool)
(declare-fun r93 () Real)
(declare-fun v842 () Bool)
(declare-fun r92 () Real)
(push 1)
(declare-fun v841 () Bool)
(declare-fun r91 () Real)
(declare-fun r90 () Real)
(push 1)
(declare-fun v840 () Bool)
(declare-fun v84 () Bool)
(declare-fun v839 () Bool)
(declare-fun r89 () Real)
(push 1)
(declare-fun v838 () Bool)
(declare-fun v837 () Bool)
(declare-fun v836 () Bool)
(push 1)
(declare-fun v835 () Bool)
(declare-fun r88 () Real)
(push 1)
(declare-fun v834 () Bool)
(declare-fun r87 () Real)
(declare-fun v833 () Bool)
(declare-fun r69 () Real)
(declare-fun v832 () Bool)
(declare-fun v824 () Bool)
(pop 1)
(declare-fun v834 () Bool)
(declare-fun r87 () Real)
(declare-fun v833 () Bool)
(pop 1)
(declare-fun v835 () Bool)
(declare-fun r88 () Real)
(declare-fun v834 () Bool)
(pop 1)
(declare-fun v838 () Bool)
(push 1)
(declare-fun v837 () Bool)
(declare-fun r88 () Real)
(declare-fun r87 () Real)
(pop 1)
(declare-fun v837 () Bool)
(declare-fun r88 () Real)
(push 1)
(declare-fun v836 () Bool)
(pop 1)
(declare-fun v836 () Bool)
(declare-fun r87 () Real)
(push 1)
(declare-fun v835 () Bool)
(declare-fun r69 () Real)
(declare-fun v834 () Bool)
(pop 1)
(declare-fun v835 () Bool)
(declare-fun v834 () Bool)
(declare-fun r69 () Real)
(pop 1)
(declare-fun v840 () Bool)
(declare-fun v84 () Bool)
(declare-fun r89 () Real)
(push 1)
(declare-fun v839 () Bool)
(push 1)
(declare-fun v838 () Bool)
(declare-fun v837 () Bool)
(pop 1)
(declare-fun v838 () Bool)
(declare-fun r88 () Real)
(pop 1)
(declare-fun v839 () Bool)
(pop 1)
(declare-fun v841 () Bool)
(pop 1)
(declare-fun v845 () Bool)
(declare-fun v844 () Bool)
(declare-fun v843 () Bool)
(declare-fun v842 () Bool)
(declare-fun r93 () Real)
(declare-fun r92 () Real)
(declare-fun v841 () Bool)
(declare-fun v840 () Bool)
(declare-fun r91 () Real)
(declare-fun v84 () Bool)
(pop 1)
(declare-fun v849 () Bool)
(declare-fun v848 () Bool)
(declare-fun v847 () Bool)
(declare-fun r93 () Real)
(declare-fun v846 () Bool)
(declare-fun v845 () Bool)
(pop 1)
(declare-fun v85 () Bool)
(declare-fun v849 () Bool)
(declare-fun r93 () Real)
(declare-fun v848 () Bool)
(declare-fun r92 () Real)
(declare-fun v847 () Bool)
(declare-fun v846 () Bool)
(declare-fun r91 () Real)
(assert (= v16 (= v16 v1) (xor true v1 true true) false))
(declare-fun v845 () Bool)
(declare-fun r90 () Real)
(declare-fun v844 () Bool)
(declare-fun v843 () Bool)
(declare-fun v842 () Bool)
(pop 1)
(push 1)
(declare-fun v99 () Bool)
(declare-fun v98 () Bool)
(push 1)
(declare-fun v97 () Bool)
(declare-fun r99 () Real)
(declare-fun r98 () Real)
(pop 1)
(declare-fun v97 () Bool)
(declare-fun v96 () Bool)
(declare-fun r99 () Real)
(push 1)
(declare-fun v95 () Bool)
(push 1)
(declare-fun v94 () Bool)
(pop 1)
(declare-fun v94 () Bool)
(declare-fun r98 () Real)
(declare-fun v93 () Bool)
(declare-fun r97 () Real)
(push 1)
(declare-fun v92 () Bool)
(declare-fun r96 () Real)
(declare-fun v91 () Bool)
(declare-fun r95 () Real)
(declare-fun v90 () Bool)
(declare-fun r94 () Real)
(declare-fun v89 () Bool)
(push 1)
(push 1)
(declare-fun v88 () Bool)
(declare-fun v87 () Bool)
(declare-fun v86 () Bool)
(declare-fun v852 () Bool)
(pop 1)
(declare-fun v88 () Bool)
(declare-fun r93 () Real)
(declare-fun v87 () Bool)
(declare-fun r92 () Real)
(declare-fun v86 () Bool)
(declare-fun v852 () Bool)
(push 1)
(declare-fun v851 () Bool)
(declare-fun v850 () Bool)
(pop 1)
(declare-fun v851 () Bool)
(declare-fun v850 () Bool)
(declare-fun r91 () Real)
(declare-fun r90 () Real)
(declare-fun v85 () Bool)
(declare-fun v849 () Bool)
(declare-fun v848 () Bool)
(declare-fun v847 () Bool)
(push 1)
(declare-fun v846 () Bool)
(pop 1)
(declare-fun v846 () Bool)
(push 1)
(declare-fun v845 () Bool)
(declare-fun r89 () Real)
(declare-fun v844 () Bool)
(pop 1)
(declare-fun v845 () Bool)
(declare-fun v844 () Bool)
(declare-fun v843 () Bool)
(declare-fun v842 () Bool)
(declare-fun v841 () Bool)
(declare-fun r89 () Real)
(pop 1)
(declare-fun v88 () Bool)
(declare-fun r93 () Real)
(declare-fun r92 () Real)
(declare-fun v87 () Bool)
(declare-fun r91 () Real)
(pop 1)
(declare-fun v92 () Bool)
(pop 1)
(declare-fun v95 () Bool)
(declare-fun r98 () Real)
(declare-fun v94 () Bool)
(declare-fun v93 () Bool)
(declare-fun v92 () Bool)
(declare-fun r97 () Real)
(declare-fun v91 () Bool)
(declare-fun v90 () Bool)
(declare-fun v89 () Bool)
(push 1)
(declare-fun v88 () Bool)
(declare-fun v87 () Bool)
(declare-fun v86 () Bool)
(declare-fun v852 () Bool)
(push 1)
(declare-fun v851 () Bool)
(declare-fun v850 () Bool)
(pop 1)
(pop 1)
(declare-fun v88 () Bool)
(declare-fun v87 () Bool)
(declare-fun v86 () Bool)
(declare-fun r96 () Real)
(declare-fun v852 () Bool)
(declare-fun v851 () Bool)
(declare-fun v850 () Bool)
(declare-fun r95 () Real)
(declare-fun r94 () Real)
(declare-fun v85 () Bool)
(declare-fun v849 () Bool)
(declare-fun r93 () Real)
(declare-fun r92 () Real)
(declare-fun v848 () Bool)
(declare-fun v847 () Bool)
(declare-fun v846 () Bool)
(declare-fun r91 () Real)
(declare-fun v845 () Bool)
(declare-fun r90 () Real)
(declare-fun v844 () Bool)
(declare-fun v843 () Bool)
(declare-fun r89 () Real)
(push 1)
(declare-fun v842 () Bool)
(declare-fun r88 () Real)
(pop 1)
(declare-fun v842 () Bool)
(declare-fun v841 () Bool)
(push 1)
(declare-fun v840 () Bool)
(declare-fun v84 () Bool)
(declare-fun r88 () Real)
(push 1)
(declare-fun v839 () Bool)
(declare-fun v838 () Bool)
(push 1)
(declare-fun v837 () Bool)
(push 1)
(declare-fun r87 () Real)
(declare-fun v836 () Bool)
(push 1)
(declare-fun v835 () Bool)
(pop 1)
(declare-fun v835 () Bool)
(declare-fun r69 () Real)
(pop 1)
(declare-fun v836 () Bool)
(push 1)
(declare-fun r87 () Real)
(pop 1)
(declare-fun v835 () Bool)
(push 1)
(declare-fun v834 () Bool)
(declare-fun v833 () Bool)
(pop 1)
(declare-fun v834 () Bool)
(declare-fun v833 () Bool)
(pop 1)
(declare-fun v837 () Bool)
(push 1)
(declare-fun r87 () Real)
(pop 1)
(declare-fun v836 () Bool)
(push 1)
(declare-fun r87 () Real)
(declare-fun v835 () Bool)
(declare-fun v834 () Bool)
(declare-fun r69 () Real)
(declare-fun v833 () Bool)
(declare-fun v832 () Bool)
(push 1)
(declare-fun v824 () Bool)
(declare-fun v823 () Bool)
(declare-fun v822 () Bool)
(push 1)
(declare-fun v821 () Bool)
(pop 1)
(declare-fun v821 () Bool)
(declare-fun v820 () Bool)
(declare-fun v819 () Bool)
(push 1)
(declare-fun v818 () Bool)
(declare-fun r359 () Real)
(pop 1)
(declare-fun v818 () Bool)
(push 1)
(declare-fun v817 () Bool)
(declare-fun v816 () Bool)
(declare-fun r359 () Real)
(pop 1)
(declare-fun v817 () Bool)
(declare-fun r359 () Real)
(declare-fun v816 () Bool)
(declare-fun r358 () Real)
(pop 1)
(declare-fun v824 () Bool)
(declare-fun r359 () Real)
(pop 1)
(declare-fun v835 () Bool)
(declare-fun r87 () Real)
(declare-fun r69 () Real)
(declare-fun v834 () Bool)
(declare-fun r359 () Real)
(declare-fun v833 () Bool)
(declare-fun r358 () Real)
(push 1)
(declare-fun v832 () Bool)
(push 1)
(declare-fun v824 () Bool)
(pop 1)
(declare-fun v824 () Bool)
(pop 1)
(declare-fun v832 () Bool)
(declare-fun r357 () Real)
(declare-fun r356 () Real)
(declare-fun v824 () Bool)
(pop 1)
(pop 1)
(declare-fun v840 () Bool)
(push 1)
(declare-fun v84 () Bool)
(declare-fun r88 () Real)
(declare-fun v839 () Bool)
(push 1)
(declare-fun v838 () Bool)
(declare-fun r87 () Real)
(push 1)
(declare-fun v837 () Bool)
(declare-fun v836 () Bool)
(declare-fun r69 () Real)
(declare-fun v835 () Bool)
(pop 1)
(pop 1)
(declare-fun v838 () Bool)
(push 1)
(declare-fun v837 () Bool)
(declare-fun r87 () Real)
(pop 1)
(declare-fun v837 () Bool)
(push 1)
(declare-fun v836 () Bool)
(push 1)
(declare-fun v835 () Bool)
(declare-fun r87 () Real)
(declare-fun v834 () Bool)
(pop 1)
(declare-fun v835 () Bool)
(declare-fun r87 () Real)
(declare-fun v834 () Bool)
(pop 1)
(declare-fun v836 () Bool)
(declare-fun v835 () Bool)
(declare-fun v834 () Bool)
(declare-fun r87 () Real)
(push 1)
(declare-fun v833 () Bool)
(declare-fun v832 () Bool)
(declare-fun v824 () Bool)
(declare-fun r69 () Real)
(declare-fun v823 () Bool)
(declare-fun v822 () Bool)
(declare-fun v821 () Bool)
(declare-fun r359 () Real)
(pop 1)
(declare-fun v833 () Bool)
(declare-fun v832 () Bool)
(declare-fun r69 () Real)
(declare-fun r359 () Real)
(declare-fun v824 () Bool)
(declare-fun v823 () Bool)
(declare-fun r358 () Real)
(declare-fun v822 () Bool)
(push 1)
(declare-fun v821 () Bool)
(pop 1)
(declare-fun v821 () Bool)
(declare-fun r357 () Real)
(pop 1)
(declare-fun v84 () Bool)
(declare-fun r88 () Real)
(push 1)
(declare-fun v839 () Bool)
(pop 1)
(declare-fun v839 () Bool)
(pop 1)
(push 1)
(declare-fun v99 () Bool)
(declare-fun v98 () Bool)
(declare-fun v97 () Bool)
(push 1)
(declare-fun v96 () Bool)
(declare-fun v95 () Bool)
(declare-fun r99 () Real)
(pop 1)
(declare-fun v96 () Bool)
(declare-fun r99 () Real)
(declare-fun v95 () Bool)
(declare-fun v94 () Bool)
(declare-fun v93 () Bool)
(declare-fun r98 () Real)
(declare-fun v92 () Bool)
(declare-fun v91 () Bool)
(declare-fun v90 () Bool)
(declare-fun r97 () Real)
(declare-fun v89 () Bool)
(declare-fun v88 () Bool)
(declare-fun r96 () Real)
(push 1)
(declare-fun v87 () Bool)
(declare-fun r95 () Real)
(declare-fun v86 () Bool)
(declare-fun v852 () Bool)
(declare-fun r94 () Real)
(pop 1)
(declare-fun v87 () Bool)
(push 1)
(declare-fun r95 () Real)
(pop 1)
(declare-fun v86 () Bool)
(declare-fun v852 () Bool)
(declare-fun r95 () Real)
(declare-fun v851 () Bool)
(declare-fun r94 () Real)
(declare-fun v850 () Bool)
(declare-fun v85 () Bool)
(declare-fun r93 () Real)
(declare-fun v849 () Bool)
(declare-fun v848 () Bool)
(declare-fun v847 () Bool)
(push 1)
(declare-fun v846 () Bool)
(pop 1)
(declare-fun v846 () Bool)
(declare-fun r92 () Real)
(declare-fun v845 () Bool)
(declare-fun r91 () Real)
(declare-fun v844 () Bool)
(declare-fun r90 () Real)
(declare-fun v843 () Bool)
(declare-fun v84 () Bool)
(declare-fun r89 () Real)
(declare-fun v818 () Bool)
(declare-fun v817 () Bool)
(declare-fun r88 () Real)
(declare-fun v816 () Bool)
(declare-fun v680 () Bool)
(declare-fun r87 () Real)
(declare-fun v681 () Bool)
(declare-fun v682 () Bool)
(push 1)
(declare-fun v842 () Bool)
(push 1)
(declare-fun v841 () Bool)
(declare-fun v840 () Bool)
(declare-fun v839 () Bool)
(declare-fun r69 () Real)
(pop 1)
(declare-fun v841 () Bool)
(declare-fun r69 () Real)
(pop 1)
(declare-fun v688 () Bool)
(declare-fun r69 () Real)
(push 1)
(declare-fun v842 () Bool)
(declare-fun r359 () Real)
(pop 1)
(declare-fun v690 () Bool)
(declare-fun v691 () Bool)
(declare-fun r359 () Real)
(push 1)
(declare-fun v842 () Bool)
(declare-fun v841 () Bool)
(pop 1)
(declare-fun v694 () Bool)
(declare-fun v695 () Bool)
(push 1)
(push 1)
(declare-fun r358 () Real)
(pop 1)
(declare-fun v842 () Bool)
(declare-fun v841 () Bool)
(pop 1)
(declare-fun v700 () Bool)
(declare-fun v701 () Bool)
(declare-fun v703 () Bool)
(declare-fun r358 () Real)
(declare-fun v708 () Bool)
(declare-fun v709 () Bool)
(declare-fun v710 () Bool)
(declare-fun r357 () Real)
(declare-fun r356 () Real)
(push 1)
(declare-fun v842 () Bool)
(push 1)
(push 1)
(declare-fun v841 () Bool)
(declare-fun r355 () Real)
(declare-fun v840 () Bool)
(declare-fun v839 () Bool)
(pop 1)
(declare-fun r355 () Real)
(push 1)
(declare-fun v841 () Bool)
(declare-fun v840 () Bool)
(declare-fun v839 () Bool)
(declare-fun v838 () Bool)
(declare-fun r354 () Real)
(declare-fun v837 () Bool)
(declare-fun v836 () Bool)
(declare-fun v835 () Bool)
(pop 1)
(declare-fun v841 () Bool)
(declare-fun r354 () Real)
(declare-fun v840 () Bool)
(declare-fun r353 () Real)
(pop 1)
(declare-fun v841 () Bool)
(declare-fun v840 () Bool)
(declare-fun v839 () Bool)
(declare-fun r355 () Real)
(push 1)
(declare-fun v838 () Bool)
(push 1)
(declare-fun v837 () Bool)
(pop 1)
(declare-fun v837 () Bool)
(declare-fun v836 () Bool)
(declare-fun r354 () Real)
(declare-fun r353 () Real)
(declare-fun r352 () Real)
(pop 1)
(declare-fun r354 () Real)
(pop 1)
(declare-fun v731 () Bool)
(declare-fun r317 () Real)
(push 1)
(declare-fun v842 () Bool)
(declare-fun v841 () Bool)
(declare-fun v840 () Bool)
(push 1)
(declare-fun r355 () Real)
(push 1)
(declare-fun v839 () Bool)
(declare-fun v838 () Bool)
(declare-fun v837 () Bool)
(pop 1)
(pop 1)
(declare-fun v839 () Bool)
(declare-fun r355 () Real)
(declare-fun v838 () Bool)
(declare-fun r354 () Real)
(push 1)
(declare-fun r353 () Real)
(declare-fun v837 () Bool)
(declare-fun r352 () Real)
(pop 1)
(declare-fun v837 () Bool)
(push 1)
(declare-fun v836 () Bool)
(declare-fun v835 () Bool)
(declare-fun r353 () Real)
(declare-fun v834 () Bool)
(declare-fun v833 () Bool)
(pop 1)
(pop 1)
(declare-fun v746 () Bool)
(declare-fun r324 () Real)
(push 1)
(push 1)
(declare-fun v842 () Bool)
(push 1)
(declare-fun v841 () Bool)
(push 1)
(declare-fun v840 () Bool)
(declare-fun v839 () Bool)
(push 1)
(declare-fun r355 () Real)
(pop 1)
(declare-fun v838 () Bool)
(declare-fun v837 () Bool)
(declare-fun v836 () Bool)
(declare-fun v835 () Bool)
(declare-fun v834 () Bool)
(declare-fun v833 () Bool)
(pop 1)
(declare-fun v840 () Bool)
(declare-fun r355 () Real)
(declare-fun r354 () Real)
(declare-fun r353 () Real)
(declare-fun v839 () Bool)
(pop 1)
(declare-fun v841 () Bool)
(declare-fun r355 () Real)
(declare-fun r354 () Real)
(declare-fun v840 () Bool)
(declare-fun v839 () Bool)
(declare-fun r353 () Real)
(push 1)
(declare-fun v838 () Bool)
(declare-fun r352 () Real)
(pop 1)
(declare-fun v838 () Bool)
(declare-fun v837 () Bool)
(declare-fun v836 () Bool)
(pop 1)
(declare-fun v842 () Bool)
(declare-fun v841 () Bool)
(declare-fun v840 () Bool)
(pop 1)
(declare-fun v770 () Bool)
(declare-fun v771 () Bool)
(declare-fun r333 () Real)
(declare-fun r334 () Real)
(push 1)
(declare-fun v842 () Bool)
(declare-fun v841 () Bool)
(push 1)
(declare-fun r355 () Real)
(declare-fun v840 () Bool)
(declare-fun v839 () Bool)
(pop 1)
(declare-fun v840 () Bool)
(push 1)
(declare-fun v839 () Bool)
(pop 1)
(declare-fun v839 () Bool)
(declare-fun v838 () Bool)
(declare-fun r355 () Real)
(push 1)
(declare-fun v837 () Bool)
(push 1)
(declare-fun v836 () Bool)
(declare-fun r354 () Real)
(declare-fun v835 () Bool)
(declare-fun v834 () Bool)
(declare-fun v833 () Bool)
(declare-fun r353 () Real)
(declare-fun v832 () Bool)
(declare-fun v824 () Bool)
(declare-fun r352 () Real)
(declare-fun v823 () Bool)
(declare-fun v822 () Bool)
(declare-fun r350 () Real)
(declare-fun v821 () Bool)
(declare-fun v820 () Bool)
(declare-fun v819 () Bool)
(declare-fun r349 () Real)
(pop 1)
(declare-fun r354 () Real)
(declare-fun v836 () Bool)
(declare-fun v835 () Bool)
(pop 1)
(declare-fun v837 () Bool)
(pop 1)
(declare-fun v821 () Bool)
(declare-fun r350 () Real)
(declare-fun v820 () Bool)
(declare-fun v819 () Bool)
(push 1)
(declare-fun r355 () Real)
(declare-fun v842 () Bool)
(push 1)
(declare-fun v841 () Bool)
(push 1)
(declare-fun v840 () Bool)
(push 1)
(declare-fun v839 () Bool)
(declare-fun r354 () Real)
(push 1)
(declare-fun v838 () Bool)
(declare-fun v837 () Bool)
(pop 1)
(declare-fun v838 () Bool)
(declare-fun r353 () Real)
(push 1)
(declare-fun v837 () Bool)
(push 1)
(declare-fun r352 () Real)
(push 1)
(declare-fun v836 () Bool)
(declare-fun v835 () Bool)
(pop 1)
(declare-fun v836 () Bool)
(pop 1)
(declare-fun v836 () Bool)
(declare-fun v835 () Bool)
(declare-fun v834 () Bool)
(declare-fun v833 () Bool)
(declare-fun v832 () Bool)
(pop 1)
(declare-fun v837 () Bool)
(declare-fun r352 () Real)
(pop 1)
(declare-fun v839 () Bool)
(pop 1)
(declare-fun v840 () Bool)
(declare-fun r354 () Real)
(declare-fun v839 () Bool)
(declare-fun v838 () Bool)
(pop 1)
(declare-fun v841 () Bool)
(pop 1)
(declare-fun v837 () Bool)
(declare-fun v823 () Bool)
(declare-fun v824 () Bool)
(assert (= v99 (or v99 (=> (= v16 (= v16 v1) (xor true v1 true true) false) v99))))
(declare-fun v832 () Bool)
(declare-fun v833 () Bool)
(declare-fun r352 () Real)
(declare-fun v834 () Bool)
(declare-fun v835 () Bool)
(declare-fun r353 () Real)
(declare-fun v836 () Bool)
(push 1)
(declare-fun v842 () Bool)
(pop 1)
(declare-fun v838 () Bool)
(declare-fun r354 () Real)
(declare-fun v839 () Bool)
(declare-fun v840 () Bool)
(declare-fun v841 () Bool)
(declare-fun v842 () Bool)
(declare-fun r355 () Real)
(pop 1)
(declare-fun v99 () Bool)
(declare-fun r99 () Real)
(declare-fun v98 () Bool)
(declare-fun r98 () Real)
(declare-fun v97 () Bool)
(declare-fun v96 () Bool)
(declare-fun v95 () Bool)
(declare-fun v94 () Bool)
(declare-fun v93 () Bool)
(declare-fun v92 () Bool)
(declare-fun r97 () Real)
(declare-fun v91 () Bool)
(declare-fun v90 () Bool)
(declare-fun r96 () Real)
(assert (and (= r99 1.0) (= 1.0 (- r99))))
